Section: New Results

Security APIs

Participants : Stéphanie Delaune, Steve Kremer, Robert Künnemann, Graham Steel, Yusuke Kawamoto, Joe-Kai Tsay.

Security APIs allow untrusted code to access sensitive resources in a secure way. The idea is to design an interface between a trusted component, such as a smart card or cryptographic security module, and the untrusted outside world such that no matter what sequence of commands in the interface are called, and no matter what the parameters, certain  good  properties will continue to hold, e.g. the secret long term keys on the smartcard are never revealed. Designing such interfaces is very tricky, and several vulnerabilities in APIs in common use have come to light in recent years.

The members of the SECSI team have been studying the application of formal security analysis techniques to APIs, for the last few years. These APIs include industrial standards such as PKCS#11 and the Trusted Platform Module (TPM).

In [37] , Delaune, Kremer and Steel present a Horn-clause-based framework for analyzing security protocols that use platform configuration registers (PCRs), which are registers for maintaining state inside the Trusted Platform Module (TPM). In their model, the PCR state space is unbounded, and experience shows that a naïve analysis using verification tools such as ProVerif or SPASS does not terminate. To address this, the authors extract a set of instances of the Horn clauses of the model, for which ProVerif does terminate on the chosen examples. The authors prove the soundness of this extraction process: no attacks are lost, that is, any query derivable in the more general set of clauses is also derivable from the extracted instances. The effectiveness of this framework is demonstrated in two case studies: a simplified version of Microsoft Bitlocker, and a digital envelope protocol that allows a user to choose whether to perform a decryption, or to verifiably renounce the ability to perform the decryption.

One of the reasons for the existence of security flaws that the members of the SECSI team identified when studying security APIs is the absence of definitions stating the expected security properties.

In [40] , Kremer, Steel and Warinschi propose a much-needed formal definition of security for cryptographic key management APIs. The advantages of this definition are that it is general, intuitive, and applicable to security proofs in both symbolic and computational models of cryptography. This definition relies on an idealized API which allows only the most essential functions for generating, exporting and importing keys, and takes into account dynamic corruption of keys. Based on this the authors can define the security of more expressive APIs which support richer functionality. They illustrate their approach by showing the security of APIs both in symbolic and computational models.

More recently, Kremer, Künnemann and Steel go even a step further in that direction and present the first key-management functionality in Canetti's Universal Composability (UC) framework. It allows one to enforce a wide range of security policy and is highly extensible. The authors illustrate its use by proving an implementation of a Security API secure with respect to arbitrary key-usage operations and explore a proof technique that allows to store cryptographic keys externally, a novelty in the UC framework. This work is currently submitted.

In other recent work, in collaboration with Riccardo Focardi at the University of Venice, Kawamoto, Steel and Tsay have investigated the error behaviour of functions in the PKCS#11 API of various cryptographic devices including security tokens, electronic ID cards and Hardware Security Modules (HSMs). In certain circumstances attackers can take advantage of errors reported to make cryptanalytic attacks on functions in the API. Taking the example of the command used to import and encrypted key onto the device, they have discovered a number of so-called `error oracle attacks' based on variations of well-known padding attacks due to Bleichenbacher and Vaudenay. This work has also recently been submitted. A number of vulnerability reports have been sent to manufacturers and national agencies.